[Merged by Bors] - feat: cardinality of Hahn series inverse by vihdzp · Pull Request #32643 · leanprover-community/mathlib4

vihdzp · 2025-12-09T10:51:21Z

depends on: [Merged by Bors] - feat: cardinality of Hahn series #32640
depends on: [Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) #32645

github-actions · 2025-12-09T10:52:26Z

PR summary c96081d930

Import changes exceeding 2%

%	File
+2.21%	`Mathlib.RingTheory.HahnSeries.Cardinal`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.HahnSeries.Cardinal	858	877	+19 (+2.21%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.HahnSeries.Cardinal`	19

Declarations diff

+ cardSupp_div_le
+ cardSupp_hsum_le
+ cardSupp_hsum_powers_le
+ cardSupp_inv_le
+ cardSupp_mul_single_le
+ cardSupp_one
+ cardSupp_one_le
+ cardSupp_pow_le
+ cardSupp_single_mul_le
+ coeff_mul_single
+ coeff_order_eq_zero
+ coeff_single_mul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

This reverts commit 2495d85.

mathlib4-merge-conflict-bot · 2025-12-10T09:59:45Z

This pull request has conflicts, please merge master and resolve them.

mathlib4-dependent-issues-bot · 2025-12-22T20:37:38Z

This PR/issue depends on:

~~[Merged by Bors] - feat: cardinality of Hahn series #32640~~
~~[Merged by Bors] - feat(SetTheory/Cardinal): formulas for sum (fun n : ℕ ↦ x ^ n) #32645~~
By Dependent Issues (🤖). Happy coding!

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

YaelDillies

Why does cardSupp exist? I am worried that we are adding API to a useless wrapper.

vihdzp · 2025-12-25T16:09:09Z

κ-bounded Hahn series appear quite a bit in the literature. In particular, the surreals are univ-bounded (small) real Hahn series with their order dual as value group.

The next PR in this series defines the subfield of κ-bounded Hahn series for uncountable κ, on which some 2,000 lines of code on the CGT repo currently depend.

YaelDillies · 2025-12-25T17:54:20Z

Great! so \kappa-bounded Hahn series is a useful concept. What I think is a useless concept that of the cardinality of a Hahn series, in the sense that it is merely the cardinality of its support.

In the PR introducing cardSupp, I see you argued that cardinalMk_support was poor naming, and that introducing cardSupp would fix that. But that argument assumed that one would write Cardinal.mk (HahnSeries.support x), while in fact it should be Set.card (HahnSeries.support x), whose name in lemmas would be card_support, which I find perfectly acceptable. If that's still too long for you, then I would advise renaming HahnSeries.support to HahnSeries.supp instead of adding cardSupp.

vihdzp · 2025-12-25T18:09:24Z

I don't believe Set.card is a thing? I've been under the impression that the way to write the cardinality of a set is to use Cardinal.mk directly.

As for renaming support to supp, this would run counter to what we do for Function.support, Polynomial.support, Module.support, Equiv.Perm.support, and PMF.support.

vihdzp · 2025-12-26T20:21:20Z

Is there any harm in having cardSupp if it is in fact an object of interest within the theory of Hahn series? Or should I rewrite this entire file in terms of cardinalMk_support?

erdOne · 2025-12-27T19:15:27Z

I don't think cardSupp is an unuseful wrapper. I think this PR and the previous PR already demonstrated that there are enough results about this idea that it warrants special API support, and having this wrapper is useful in pointing people to these API.
Other than this issue I think this PR is ready to go and I think some third opinion here to unblock this PR would be useful.

maintainer merge?

github-actions · 2025-12-27T19:15:37Z

🚀 Pull request has been placed on the maintainer queue by erdOne.

jcommelin

Thanks 🎉

bors merge

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

mathlib-bors · 2026-01-02T14:04:24Z

Pull request successfully merged into master.

Build succeeded!

And happy new year! 🎉

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

vihdzp added 8 commits December 9, 2025 02:12

start

6b855a2

more stuff

a530fad

this seems sufficient

1b69fc2

Update Mathlib.lean

9239676

only need this atm

39cc03e

ctue

92cf621

mb

1a8cfb3

there

73b8420

github-actions bot added the t-ring-theory Ring theory label Dec 9, 2025

vihdzp added 2 commits December 9, 2025 04:54

more

b8ac712

prove

7146db2

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 9, 2025

vihdzp added 5 commits December 9, 2025 05:35

add zero case

320f1c1

Update Cardinal.lean

4dbb1b7

Merge branch 'card' into hahnsize2

3bf3bce

fix

feed359

Update Arithmetic.lean

3b70c32

vihdzp mentioned this pull request Dec 9, 2025

[Merged by Bors] - feat: subfield of Hahn series bounded by a cardinal #32648

Closed

1 task

vihdzp added 5 commits December 9, 2025 06:16

private import

2495d85

Update Cardinal.lean

cc1dd49

Update Cardinal.lean

858cd1a

Update Cardinal.lean

fe9b73f

Revert "private import"

8bda184

This reverts commit 2495d85.

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2025

vihdzp added 2 commits December 10, 2025 04:09

Merge branch 'master' into hahnsize

478cdaf

Merge branch 'hahnsize' into hahnsize2

ef3d328

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 10, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 11, 2025

Update Mathlib/RingTheory/HahnSeries/Cardinal.lean

98ee14e

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 22, 2025

Merge branch 'master' into hahnsize2

7fabd61

vihdzp requested a review from wwylele December 22, 2025 21:08

vihdzp added 2 commits December 22, 2025 16:01

Refactor HahnSeries to use R⟦Γ⟧ type

f6b0c15

Update Multiplication.lean

2ae5ac7

wwylele approved these changes Dec 23, 2025

View reviewed changes

Comment thread Mathlib/RingTheory/HahnSeries/Cardinal.lean Outdated

Comment thread Mathlib/RingTheory/HahnSeries/Cardinal.lean Outdated

Apply suggestions from code review

0f193eb

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

vihdzp requested a review from YaelDillies December 25, 2025 00:48

YaelDillies reviewed Dec 25, 2025

View reviewed changes

leanprover-community-bot-assistant assigned mariainesdff Dec 26, 2025

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 27, 2025

jcommelin reviewed Jan 2, 2026

View reviewed changes

mathlib-bors bot pushed a commit that referenced this pull request Jan 2, 2026

feat: cardinality of Hahn series inverse (#32643)

f668f45

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 2, 2026

mathlib-bors bot changed the title ~~feat: cardinality of Hahn series inverse~~ [Merged by Bors] - feat: cardinality of Hahn series inverse Jan 2, 2026

mathlib-bors bot closed this Jan 2, 2026

kim-em pushed a commit to kim-em/mathlib4 that referenced this pull request Jan 6, 2026

feat: cardinality of Hahn series inverse (leanprover-community#32643)

9c71e18

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

adomani mentioned this pull request Jan 16, 2026

feat: MiM PR report #15355

Open

goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026

feat: cardinality of Hahn series inverse (leanprover-community#32643)

1a7c80e

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

vihdzp deleted the hahnsize2 branch March 13, 2026 23:23

Conversation

vihdzp commented Dec 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c96081d930

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-merge-conflict-bot commented Dec 10, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Dec 22, 2025

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

vihdzp commented Dec 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Dec 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

vihdzp commented Dec 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

vihdzp commented Dec 26, 2025

Uh oh!

erdOne commented Dec 27, 2025

Uh oh!

github-actions bot commented Dec 27, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 2, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

vihdzp commented Dec 9, 2025 •

edited

Loading

github-actions bot commented Dec 9, 2025 •

edited

Loading

vihdzp commented Dec 25, 2025 •

edited

Loading

YaelDillies commented Dec 25, 2025 •

edited

Loading

vihdzp commented Dec 25, 2025 •

edited

Loading